Nuprl Lemma : eq_id_self
11,40
postcript
pdf
a
:Id. sqequal(eq_id(
a
;
a
); tt)
latex
Definitions
x
:
A
.
B
(
x
)
,
eq_id(
a
;
b
)
,
t
T
,
sq_type(
T
)
,
P
Q
,
guard(
T
)
Lemmas
eqof
eq
btrue
,
Id
wf
,
id-deq
wf
,
btrue
wf
,
bool
sq
origin
a:Id. sqequal(eq_id(a; a); tt) a:Id. sqequal(eq_id(a; a); tt) x:A. B(x)
T
Q